Section: Software

Memevents-Litmus-Diy-Dont

Participants : Jade Alglave, Luc Maranget [correspondant] , Susmit Sarkar [U. of Cambridge, UK] , Peter Sewell [U. of Cambridge, UK] .

Luc Maranget is the main developer of the tools suite of project “Weak Memory Models” (cf. the relevant section).

This suite features three subtools memevents (model checker), litmus (runs tests on actual machines) and diy (generate tests from concise specifications). This year saw a new tool and one official releases (with documentation) [33] — see also http://diy.inria.fr . The releases feature all tools except memevents, which we wish to keep for ourselves.

This year main extensions are the handling of the ARM architecture and more collaboration between tools. For the latter, the test generator diy enrichs tests with meta-data that are exploited by litmus, so as to perform binding of test threads to machine processors, intelligent prefetch of data etc. We plan a new release of the tool suiteearly next year.

A new, independant, “proof of concept” tool, offence was written by J. Alglave and L. Maranget, as a support of our publication [30] .

This software is available at http://diy.inria.fr/offence .